\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$), $z$:Top, $L_{1}$,\+
\\[0ex]$L_{2}$:Top List.
\-\\[0ex]ecl{-}trans{-}state{-}from($v$;$z$;$L_{1}$ @ $L_{2}$)
\\[0ex]$\sim$
\\[0ex]ecl{-}trans{-}state{-}from($v$;ecl{-}trans{-}state{-}from($v$;$z$;$L_{1}$);$L_{2}$)
\end{tabbing}